i, a:Id, p:FinProbSpace, ds:x:Id fp Type, P:(State(ds)).
@i (with ds: ds action a:p precondition a is P s)  Dsys 

latex

Definitions	Id, t  T, FinProbSpace, Type, x. t(x), x:A. B(x), a:A fp B(a), , State(ds), x:AB(x), , (precondition a:Outcome(p) is P:State(ds) -> Bool), MsgA, IdDeq, eqof(d), f(a), if b then t else f fi , x.A(x), @i (with ds: ds action a:T precondition a is P s), Dsys
Lemmas	ifthenelse wf, eqof wf, id-deq wf, msga wf, ma-single-pre wf, ma-empty wf, ma-state wf, bool wf, fpf wf, finite-prob-space wf, Id wf